/**
 * 
 */
package IC.Analyzer;

import java.util.List;
import IC.AST.*;
import IC.AST.nodes.*;
import IC.Analyzer.Types.*;

/**
 * Checks that the types of all expressions match (add implemented
 * rules here):
 * 1. used variables are defined
 * 2. [] are used with arrays and integer indices
 * 3. referenced memeber variables exist
 * 4. .length is taken from arrays only
 * 5. the "new <type>[<n>]" expression is with a valid type and integer size
 * 6. the "new <class-id>()" expression is with a valid class id 
 * 7. `this` is defined where used
 * 8. assignments are from subtype to supertype
 * 9. if conditions are boolean
 * 10. while conditions are boolean
 * 11. return statements in a function match function return types
 * 12. variable initiallization is with appropriate type
 * 13. binary expressions operands are of appropriate types (5 cases)
 * 14. unary expressions
 * 15. static call argument types, argument list size match method definitions,
 * 		class and method exist.
 * 16. virtual call argument types, argument list size match method definitions,
 * 		class instance and method exist.
 * 
 * Up -> Type
 * Down -> Object 
 * 
 * propogate null to ignore and recover from errors
 * 
 */
public class TypeChecker extends Checker<Object,Type> 
implements PropogatingVisitor<Object,Type> {

	public TypeChecker(ASTNode root) throws Exception {
		recoverErrors();
		root.accept(this, null);
		if (hadError()) {
			throw new SemanticError(root,"program is incorrect");
		}
	}

	/* literals - no checks needed, just set and return type */
	public Type visit(BoolLiteral that, Object d) throws Exception {
		that.setType(BoolType.getIt());
		return that.getType();
	}

	public Type visit(IntLiteral that, Object d) throws Exception {
		that.setType(IntType.getIt());
		return that.getType();
	}

	public Type visit(NullLiteral that, Object d) throws Exception {
		that.setType(NullType.getIt());
		return that.getType();
	}

	public Type visit(StringLiteral that, Object d) throws Exception {
		that.setType(StringType.getIt());
		return that.getType();
	}

	/* variables (l-values) - symtab lookup */
	/**
	 * rule 2
	 */
	public Type visit(ArrayElmVar that, Object d) throws Exception {
		Type arrT = that.getArray().accept(this,d);
		Type indexT = that.getIndex().accept(this,d);

		// check array specifier
		if (! (arrT instanceof ArrayType))
			error(that,"cannot index a non-array expression");

		// check index specifier
		if (indexT !=null &&! indexT.isSubtypeOf(IntType.getIt()))
			error(that,"non-integer array index");
		try{
			that.setType(((ArrayType)arrT).getElmType());
		}
		catch(ClassCastException e){}
		return that.getType();
	}

	/**
	 * rule 1
	 */
	public Type visit(SimpleVar that, Object d) throws Exception {
		SymTable scope = that.getSymTab();
		SymTabEntry e = scope.resolve(that.getID());
		if (e == null || ! e.isVar()) {
			error(that,"undefined variable `"+that.getID()+"'");
			return null;
		}
		that.setType(e.getType());
		return that.getType();
	}

	/**
	 * rule 3
	 */
	public Type visit(MemberVar that, Object d) throws Exception {
		Type instanceT = that.getInstance().accept(this,d);
		if (! (instanceT instanceof ClassType))
			throw new SemanticError(that,"cannot take property of non-class");

		// find the class ASTnode
		ClassDecl decl = ((ClassType)instanceT).getDecl();

		// find the member var
		SymTabEntry e = decl.getSymTab().resolve(that.getID());
		if (e == null || !e.isMemberVar()) {
			error(that,"class `"+decl.getClassID()+"' has no memeber `"+that.getID()+"'");
			//error(that,"class '%s' has no memeber '%s'", new Object[]{decl.getClassID(), that.getID()});
			return null;
		}
		that.setType(e.getType());
		return that.getType();
	}

	/* expressions - deduce the types using some logic */
	/**
	 * rule 13
	 */
	public Type visit(BinaryExpr that, Object d) throws Exception {
		Type typeR = that.getLeft().accept(this,d);
		Type typeL = that.getRight().accept(this,d);

		Operator op = that.getOp();
		if (typeR != null && typeL != null) 
		{
			if((typeL.isSubtypeOf(StringType.getIt())) && (typeR.isSubtypeOf(StringType.getIt()))
					&& op == Operator.PLUS) {
				that.setType(StringType.getIt());
			} 
			else if(typeL.isSubtypeOf(IntType.getIt()) && typeR.isSubtypeOf(IntType.getIt())
					&& Operator.BinaryMathOps.contains(op)) {
				that.setType(IntType.getIt());
			}
			else if(typeL.isSubtypeOf(IntType.getIt()) && typeR.isSubtypeOf(IntType.getIt())
					&& Operator.LtGtOps.contains(op)) {
				that.setType(BoolType.getIt());
			}
			else if(typeL.isSubtypeOf(BoolType.getIt()) && typeR.isSubtypeOf(BoolType.getIt())
					&& Operator.AndOrOps.contains(op)){
				that.setType(BoolType.getIt());
			}
			else if((verifyTypes(that, typeL, typeR) ||
					verifyTypes(that, typeR, typeL)) &&
					Operator.EqNEqOps.contains(op)) {
				that.setType(BoolType.getIt());
			}
			else {
				error(that,"cannot perform binary operation " + 
						op + " on these types: " + typeR + ", " + typeL);
				return null;
			}
		}
		return that.getType();
	}

	/**
	 * rule 14
	 */
	public Type visit(UnaryExpr that, Object d) throws Exception {
		Type operandT = that.getOperand().accept(this,d);
		Operator op = that.getOp();

		if (operandT.isSubtypeOf(IntType.getIt()) && op.equals(Operator.MINUS)) {
			that.setType(IntType.getIt());
		} 
		else if(operandT.isSubtypeOf(BoolType.getIt()) && op.equals(Operator.LNEG)){
			that.setType(BoolType.getIt());
		}
		else {
			error(that, "unary operator unsupported on expression of type '" + operandT.toString() + "'");
			return null;
		}
		return that.getType();
	}

	/**
	 * rule 4
	 */
	public Type visit(LengthExpr that, Object d) throws Exception {
		Type arrT = that.getArray().accept(this,d);
		if (! (arrT instanceof ArrayType))
			error(that,"cannot take length of a non-array expression");
		that.setType(IntType.getIt());
		return that.getType();
	}

	/**
	 * rule 5
	 */
	public Type visit(NewArrayExpr that, Object d) throws Exception {
		Type elmType = that.getElemType().getType();
		if (that.getSize() != null) {
			Type sizeT = that.getSize().accept(this,d);
			verifyTypes(that,sizeT,IntType.getIt());
		}
		that.setType(ArrayType.getIt(elmType));
		return that.getType();
	}

	/**
	 * rule 6
	 */
	public Type visit(NewClassExpr that, Object d) throws Exception {
		SymTabEntry e = that.getSymTab().resolve(that.getClassID());
		if (e == null || ! e.isClass()) {
			error(that,"the class `"+that.getClassID()+"' is undefined");
			return null;
		}
		that.setType(e.getType());
		return that.getType();
	}

	/**
	 * rule 7
	 */
	public Type visit(ThisExpr that, Object d) throws Exception {
		SymTabEntry e = that.getSymTab().resolve("this");
		if (e == null || !e.isThis()) {
			error(that,"`this' is undefined here");
			return null;
		}
		that.setType(e.getType());
		return that.getType();
	}

	/* method calls - validate argument types */
	/**
	 * rule 15
	 */
	public Type visit(StaticCall that, Object d) throws Exception {

		SymTable scope = that.getSymTab();
		SymTabEntry classEntry = scope.resolve(that.getClassID());
		if(classEntry == null || !classEntry.isClass()) {
			error(that, "undefined class `" + that.getClassID() + "'");
			return null;
		} 

		ClassDecl declNode = (ClassDecl)classEntry.getDeclNode();
		SymTable staticScope = declNode.getStaticSymTab();
		SymTabEntry methEntry = staticScope.resolve(that.getMethodID());
		if (methEntry == null || !methEntry.isStaticMethod()) {
			error(that, "undefined static method `" + that.getMethodID() + "'");
			return null;
		}

		MethodType methodType = (MethodType)methEntry.getType();

		// compare size of formal argument list
		List<Type> args = methodType.getArgs();
		if(args.size() != that.getArgs().size()) {
			error(that, "invalid number of arguments");
			return that.getType();
		}

		// compare type of formal arguments
		int i=0;
		for ( Expression arg : that.getArgs()) {
			Type formalType = args.get(i++);
			Type actualType = arg.accept(this,d);
			if (actualType != null)
				verifyTypes(that,actualType,formalType);
		}	
		that.setType(methodType.getRetType());
		return that.getType();
	}

	/**
	 * rule 16
	 */
	public Type visit(VirtualCall that, Object d) throws Exception {
		// find the method scope from the instance
		SymTable scope;
		if (that.getInstance() == null) {
			scope = that.getSymTab();
		} 
		else {
			try{
				ClassType instType = (ClassType)that.getInstance().accept(this,d);
				scope = instType.getDecl().getSymTab();
			}catch(ClassCastException e)
			{
				error(that, that.getMethodID() + "is a applied to an undefined class instance");
				return null;
			}
			catch(NullPointerException e)
			{
				return null;
			}
		}

		// check whether method exists 
		SymTabEntry entry = scope.resolve(that.getMethodID());
		if (entry == null || !entry.isVirtualMethod()) {
			error(that, "undefined virtual method `" + that.getMethodID() + "'");
			return null;
		}
		else {
			MethodType methodType = (MethodType)entry.getType();

			// compare size of formal argument list
			List<Type> args = methodType.getArgs();
			if(args.size() != that.getArgs().size()) {
				error(that, "invalid number of arguments");
			}

			// compare type of formal arguments
			int i=0;
			for ( Expression arg : that.getArgs()) {
				Type formalType = args.get(i++);
				Type actualType = arg.accept(this,d);
				if (actualType != null)
					verifyTypes(that,actualType,formalType);
			}
			that.setType(methodType.getRetType());
			return that.getType();
		}
	}

	/* statements - verify the types match the expected types in the statement */
	/**
	 * rule 8
	 */
	public Type visit(AssignStmt that, Object d) throws Exception {
		Type srcT = that.getSrc().accept(this,d);
		Type dstT = that.getDest().accept(this,d);
		if (srcT != null && dstT != null)
			verifyTypes(that,srcT,dstT);
		return null;
	}

	/**
	 * rule 9
	 */
	public Type visit(IfStmt that, Object d) throws Exception {
		// check that condition is boolean
		Type condT = that.getCondition().accept(this,d);
		Type bool = BoolType.getIt();
		if (condT != null && bool != null){
			verifyTypes(that,condT,bool);

			// check statements
			that.getIfStmt().accept(this,d);
			if (that.getElseStmt() != null) {
				that.getElseStmt().accept(this,d);
			}
		}
		return null;
	}

	/**
	 * rule 10
	 */
	public Type visit(WhileStmt that, Object d) throws Exception {
		// check that condition is boolean
		Type condT = that.getCondition().accept(this,d);
		Type bool = BoolType.getIt();
		if (condT != null && bool != null)
		{
			verifyTypes(that,condT,bool);
			// check statements
			that.getCondition().accept(this,d);
			that.getBody().accept(this,d);
		}
		return null;
	}

	/**
	 * rule 11
	 */
	public Type visit(ReturnStmt that, Object d) throws Exception {
		// find return expr type
		Type srcT = (that.getExpr() == null) ?
				VoidType.getIt() :	that.getExpr().accept(this,d);

		SymTabEntry e = that.getSymTab().resolve("return");
		if (e == null || ! e.isReturnType()) {
			throw new SemanticError(that,"Unexpected error");
		}
		// find function return type
		Type dstT = e.getType();
		if (srcT != null)
			verifyTypes(that,srcT,dstT);
		return null;
	}

	/** 
	 * rule 12
	 */
	public Type visit(VarDeclStmt that, Object d) throws Exception {
		if (that.getInit() != null) {
			Type srcT = that.getInit().accept(this,d); 
			Type dstT = that.getVar().accept(this,d);;
			if (srcT != null)
				verifyTypes(that,srcT,dstT);
		}
		return null;
	}


	/**
	 * throws an error if src cannot be down-casted to dst
	 * @param node
	 * @param srcT
	 * @param dstT
	 * @throws Exception
	 */
	private boolean verifyTypes(ASTNode node, Type srcT, Type dstT) throws Exception {
		if (! srcT.isSubtypeOf(dstT)) {
			error(node,"cannot convert from `"+srcT+"' to `"+dstT+"'");
			return false;
		}
		else return true;
	}

}
